(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, 1).
The TRS R consists of the following rules:
f(g(i(a, b, b'), c), d) → if(e, f(.(b, c), d'), f(.(b', c), d'))
f(g(h(a, b), c), d) → if(e, f(.(b, g(h(a, b), c)), d), f(c, d'))
Rewrite Strategy: INNERMOST
(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
g0(0, 0) → 0
i0(0, 0, 0) → 0
a0() → 0
b0() → 0
b'0() → 0
c0() → 0
d0() → 0
if0(0, 0, 0) → 0
e0() → 0
.0(0, 0) → 0
d'0() → 0
h0(0, 0) → 0
f0(0, 0) → 1
e1() → 2
b1() → 5
c1() → 6
.1(5, 6) → 4
d'1() → 7
f1(4, 7) → 3
b'1() → 10
.1(10, 6) → 9
f1(9, 7) → 8
if1(2, 3, 8) → 1
a1() → 15
b1() → 16
h1(15, 16) → 14
c1() → 17
g1(14, 17) → 13
.1(5, 13) → 12
d1() → 18
f1(12, 18) → 11
c1() → 20
f1(20, 7) → 19
if1(2, 11, 19) → 1
(2) BOUNDS(1, n^1)
(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(g(i(a, b, b'), c), d) → if(e, f(.(b, c), d'), f(.(b', c), d'))
f(g(h(a, b), c), d) → if(e, f(.(b, g(h(a, b), c)), d), f(c, d'))
Tuples:
F(g(i(a, b, b'), c), d) → c1(F(.(b, c), d'), F(.(b', c), d'))
F(g(h(a, b), c), d) → c2(F(.(b, g(h(a, b), c)), d), F(c, d'))
S tuples:
F(g(i(a, b, b'), c), d) → c1(F(.(b, c), d'), F(.(b', c), d'))
F(g(h(a, b), c), d) → c2(F(.(b, g(h(a, b), c)), d), F(c, d'))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
F(g(i(a, b, b'), c), d) → c1(F(.(b, c), d'), F(.(b', c), d'))
F(g(h(a, b), c), d) → c2(F(.(b, g(h(a, b), c)), d), F(c, d'))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(g(i(a, b, b'), c), d) → if(e, f(.(b, c), d'), f(.(b', c), d'))
f(g(h(a, b), c), d) → if(e, f(.(b, g(h(a, b), c)), d), f(c, d'))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(8) BOUNDS(1, 1)